T:Type, x, y, z:T. ((y = z))  (((x = y)  (x = z))  ((x = y))) 

latex

ProofTree

Definitions	P  Q, P & Q, P  Q, x:A. B(x), , t  T, A, False, P  Q
Lemmas	not wf